T:Type, L:(T List), R:({x:T| (x  L)} Realizer), x:T, B:Realizer.
(x  L)  xL.R(x)  B  R(x)  B 

latex

Definitions	x. t(x), t  T, P  Q, x:A. B(x), x(s),
Lemmas	R-sub-Rall, es realizer wf, R-sub wf, Rall wf, l member wf, R-sub transitivity